package dv.apkeep;

import dv.network.Device;

import java.util.HashSet;
import java.util.LinkedList;

public class Verifier {
    private DeltaForwardingGraph dfg;
    private HashSet<Property> properties;

    public Verifier(DeltaForwardingGraph dfg, HashSet<Property> properties) {
        this.dfg = dfg;
        this.properties = properties;
    }

    public LinkedList<Device> checkInvariants() {
        int result = 0;
        for (Device device : this.dfg.graph.vertexSet()) {
            if (device.getName() == "default") {
                continue;
            }
            HashSet<Integer> pset = (HashSet<Integer>) this.dfg.transferredPreds.clone();
            LinkedList<Device> history = new LinkedList<>();
            LinkedList<Device> r = this.traverse(device, pset, history);
            if (r != null) {
                return r;
            }
        }
        return null;
    }

    /**
     *
     * @param s
     * @param pset
     * @param history
     * @return history
     */
    private LinkedList<Device> traverse(Device s, HashSet<Integer> pset, LinkedList<Device> history) {
        if (pset.isEmpty()) {
            return null;
        }
        if (history.contains(s)) {
            System.out.println(System.nanoTime());
            System.out.println("loop");
            System.out.print(history);
            System.out.print(s);
            System.out.println();
            LinkedList<Device> nhistory = (LinkedList<Device>) history.clone();
            nhistory.add(s);
            return nhistory;
        }
        for (DeltaForwardingGraph.ECEdge edge : this.dfg.graph.edgesOf(s)) {
            if (edge.getFrom() == s) {
                if (edge.getTo().getName() == "default") {
                    System.out.println(System.nanoTime());
                    System.out.println("blackhole");
                    System.out.print(history);
                    System.out.print(s);
                    System.out.println();
                    LinkedList<Device> nhistory = (LinkedList<Device>) history.clone();
                    nhistory.add(s);
                    return nhistory;
                }
                HashSet<Integer> npset = (HashSet<Integer>) pset.clone();
                npset.retainAll(edge.getPredicates());
                LinkedList<Device> nhistory = (LinkedList<Device>) history.clone();
                nhistory.add(s);
                return this.traverse(edge.getTo(), npset, nhistory);
            }
        }
        return null;
    }

    public void checkReachability() {
        for (Property property: this.properties) {
            property.getAutomata().init();
            if (!this.dfg.graph.vertexSet().contains(property.getSource())) { // delta not affect source
                return;
            }
            HashSet<Integer> pset = (HashSet<Integer>) this.dfg.transferredPreds.clone();
            LinkedList<Device> history = new LinkedList<>();
            this.traverseReach(property.getSource(), pset, history, property.getAutomata());
        }

    }

    private void traverseReach(Device s, HashSet<Integer> pset, LinkedList<Device> history, Automata automata) {
        if (pset.isEmpty()) {
            return;
        }
        if (history.contains(s)) {
            System.out.println(System.nanoTime());
            System.out.println("loop");
            System.out.print(history);
            System.out.print(s);
            System.out.println();
            return;
        }
        for (DeltaForwardingGraph.ECEdge edge : this.dfg.graph.edgesOf(s)) {
            if (edge.getFrom() == s) {
                if (edge.getTo().getName() == "default") {
                    System.out.println(System.nanoTime());
                    System.out.println("blackhole");
                    return;
                }
                HashSet<Integer> npset = (HashSet<Integer>) pset.clone();
                npset.retainAll(edge.getPredicates());
                LinkedList<Device> nhistory = (LinkedList<Device>) history.clone();
                nhistory.add(s);
                try {
                    Automata automata1 = (Automata) automata.clone();
                    automata1.takeAction(s.getName());
                    this.traverseReach(edge.getTo(), npset, nhistory, automata1);
                } catch (CloneNotSupportedException e) {
                    e.printStackTrace();
                }
            }
        }
    }
}
